Benchmarking Linear Logic

Abstract: Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. The availability of such libraries of problems for non-classical logics is very limited. So in work with Olarte, Pimentel, and Reis (2018) we proposed a library for benchmarking Girard's (propositional) intuitionistic linear logic, starting from Kleene's initial collection of intuitionistic theorems. However, we want to use these theorems not for checking the efficiency of different theorem provers for the logic, but instead, I wanted to investigate the structure of the space of proofs of linear theorems, in different variants of linear logic. Having learned of Tarau's work on 'generating' intuitionistic implication theorems, I suggested to him that we could calculate the 'linear' implicational theorems. His program turned out to be very adept and in a few hours produces almost 8 billion "small" implicational linear theorems. Given this scale, we decided we could do some machine learning of intuitionistic linear logic, and the results seem impressive.

(This is joint work with Paul Tarau, presented by him at ICLP2020, CLA2020)

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/